米田の補題の証明 ⑤
前提条件などは↑を参照
①~④により、
任意の$ A\in\mathscr{A} と$ X\in[\mathscr{A}^\mathrm{op},\mathrm{Set}] について、
$ [\mathscr{A}^\mathrm{op},\mathrm{Set}](H_A, X) と$ X(A) の間に全単射を定義できた
この全単射が各$ A,Xに対して自然であることを示す
そのためには以下の2つを示さなねばならない
⑤-1: ①が自然である
⑤-2: ②が自然である
つまり、$ \spades\cong\heartsを示すために、
$ \spades,\hearts間の自然変換を定義する方法を選択するわけではなく、
各成分が同型射である
という方を選択しようとしているわけで、そうなると、$ \tilde{}と$ \hat{}で全く同じ議論を2回することになるので。
今回は⑤-1を示すことにする
つまり、関手$ \hat{}が組$ (A,X)について自然であることを示す
2変数関手の自然性を、
$ A,Xをそれぞれ固定した2つの関手の自然性を示す
ことで示す
要するに示したいことは、以下の2つである
⑤-1-1: $ \hat{}が、固定した$ Xごとに$ Aについて自然
⑤-1-2: $ \hat{}が、固定した$ Aごとに$ Xについて自然
⑤-1-1
$ \hat{}が、固定した$ Xごとに$ Aについて自然であることを示す
各$ X\in[\mathscr{A}^\mathrm{op},\mathrm{Set}](H_A, X) と、
$ \mathscr{A}の$ f:B\to Aについて
下図の可換性を言えればいい
https://gyazo.com/58c553edf1e5c6066d26326c341e2165
つまり上図の赤の部分の等式を示せばいい
$ \alphaから出発している
$ \alphaは$ H_A\to Xな自然変換mrsekut.icon
$ (\alpha\circ H_f)_B(1_B)=\alpha_B((H_f)_B(1_B))
∵$ [\mathscr{A}^\mathrm{op},\mathrm{Set}](H_A, X) における射の合成の定義
雑に言えば$ (g\circ f)(x)=g(f(x))と同じ話mrsekut.icon
$ =\alpha_B(f\circ 1_B)=\alpha_B(f)
∵ $ H_fの定義
$ =(Xf)(\alpha_A(1_A))
より、言える
⑤-1-2
$ \hat{}が、固定した$ Aごとに$ Xについて自然であることを示す
各$ A\in\mathscr{A}と、
$ [\mathscr{A}^\mathrm{op},\mathrm{Set}] の射$ \theta:X\to X'について
https://gyazo.com/5e18d1fe915ec729b9099383c804d839
この$ \thetaねmrsekut.icon
下図の可換性を言えればいい
https://gyazo.com/6c6a1eeec7bcf2dbd5b058cd092c9f2e
$ \alphaから出発している
$ \alphaは$ H_A\to Xな自然変換mrsekut.icon
$ [\mathscr{A}^\mathrm{op},\mathrm{Set}] 内の合成の定義より、$ (\theta\circ\alpha)_A=\theta_A\circ\alpha_A
より、言える